This PR contains some experimental work I've been doing to allow more precise user control over property testing. The basic idea is to make the random value generation process more programmable (taking inspiration from things like Hedgehog) by exposing a Gen monad.

Design considerations:

1. Allow more targeted value generation, e.g., to ensure that preconditions are satisfied. This helps to solve a classic problem with random testing where the user is given a false sense of confidence in their tests because all or most of their generated test vectors pass only because they do not satisfy some precondition.
2. Allow value generation code to be used uniformly in both concrete modes (which uses random generation) and in symbolic modes (which creates fresh uninterpreted variables). This is similar to how :check and :prove can currently be used uniformly on functions with appropriate types.
3. Allow methods for users to generate datatypes with internal invariants (similar to 1). I am considering disallowing newtype types to be automatically generated for :check and :prove, etc. This facility would provide a replacement for that capability that users could directly implement. If we ever implement user-definable instances for newtypes, this would further let them participate directly in the autogeneration mechanism by implementing the Generate class.
4. Stretch goal: provide methods for counterexample shrinking. Random generation can sometimes yield counterexamples that are hard to understand, and shrinking methods attempt to automatically find "smaller" counterexamples that also produce failures, under the assumption that smaller counterexamples will be easier for humans to understand. Providing this generator abstraction brings us closer to being able to implement this.

At this point, I'm seeking input about whether it is useful to continue working in this direction and thoughts about the overall design.